Nuprl Lemma : insert_wf
11,40
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
a
:
T
,
L
:(
T
List). insert(
eq
;
a
;
L
)
(
T
List)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
insert(
eq
;
a
;
L
)
Lemmas
ifthenelse
wf
,
deq-member
wf
,
deq
wf
origin
T:Type, eq:EqDecider(T), a:T, L:(T List). insert(eq; a; L) 
(T List) T:Type, eq:EqDecider(T), a:T, L:(T List). insert(eq; a; L) (T List) x:A. B(x) T